HW#3 --- last modified February 07 2019 04:20:45..

Solution set.

Due date: Nov 3

Files to be submitted:
  Hw3.zip

Purpose: To write a CSP solver for Sudoku. To learn more about logic-based agents.

Related Course Outcomes:

The main course outcomes covered by this assignment are:

LO2 -- By code or by hand translate sentences in logic to conjunctive normal form (CNF).

LO3 -- By code or by hand find proofs by using resolution.

LO7 -- Students should be able to explain the advantages and disadvantages of forward checking in constraint satisfaction.

Specification:

This homework will consist of two parts: Some written questions and a coding part. You are to write up your written questions in a file Hw3.pdf which you include as part of the zip file. Make sure to list all group members and their IDs at the top of this file. Here are the written questions:

1. Suppose we have a two person game. In a given ply, a player can make one of three moves. The value of a move for a player can be encoded in three bits, one for sign, and two to encode a number 1-4. We use the variable `V_(m_1,...,m_i,b)` to denote the `b`th bit of the value of the sequence of moves `m_1, ... m_i` to MAX. Suppose a game ends after 4 plys. Express as three propositional formulas the backed up minimax value of move 1, `V_(1,b)` for each bit `b`, in terms of the variables `V_(1,m_2,m_3,m_4,b)`. Convert these formulas to CNF.
2. The pigeonhole principle `PHP_(n)^(n+1)` says any function from `n+1` pigeons into `n` holes must result in two pigeons in the same hole. Let `P_(i,j)` be a variable expressing that pigeon `i` gets mapped to hole `j`. Consider the `n=3` case. Express the following as propositional formulas:
   1. Every `i` gets mapped to some `j`.
   2. Some `j` is mapped to by `i` and `i'` where `i ne i'`.
   The implication (a) => (b) is a propositional formula for `PHP_(3)^(4)`. Convert `neg PHP_(3)^(4)` to clausal form and give a resolution refutation for this statement. Finally, trace the execution of DPLL on this formula.

For the programming portion of this assignment, you are to write a CSP solver which will be run from the command line with a syntax like:

python csp_solver.py problem_filename use_forward_check_flag

Here problem_filename is the name of some text file containing a CSP using the syntax we now describe. use_forward_check_flag is either 1 or 0 and determines whether forward checking is used. A legal file will consists of a sequence of lines each representing one constraint. A given line has the syntax:

Variable Rel Var_Or_Integer

The separator between each item above is a single space character and a line is terminated by a newline character. A Variable is a string beginning with either a lower lower or upper case letter followed by any number of lower or upper case letters or numbers or underscores. For example,

X5   -- A variable
l33t_Pr0Gr4mm0r  -- A variable
5 -- Not a variable
$perl_nerd -- Not a variable as begins with dollars
SA  -- A variable
NSW -- A variable

Rel is one of eq, ne, lt, gt representing the equals, not equals, less than, or greater than relations. Finally, Var_Or_Integer can either be a variable or a nonnegative integer. Here are some example legal lines:

SA ne NSW
bob eq 27
Ewoks lt Yoda 

Given such a legal file, your program should first make a scan of the file to determine the number `D` of distinct variables in the file as well as the largest value `V` of an integer in a constraint. The CSP then consists of the relations given in the file where each variable has domain `0, 1, ... max(D-1,V)`. Given this CSP your program should run the backtracking procedure described in class. SELECT-UNASSIGNED VARIABLES should implement the MRV and degree heuristics, ORDER-DOMAIN-VALUES should implement the least-constraining-value heuristic. INFERENCES should either return the empty assignment or should do forward checking depending on the command line option. The output of your program should be either "NO SOLUTION" or a sequence of lines each containing one variable assignment in a solving the problem. The variables should be output in lexicographical order. You should include the test files you create for this homework in the ZIP folder. At least one of these test files should be a formulation of the map coloring of Australia problem from the book where we let red = 0, green = 1, blue = 2. Here is an example for this problem of a possible output:

NSW=2
NT=2
Q=1
SA=0
T=0
V=1
WA=1

Consider the smaller map, consisting of three countries: Shortz -- as it looks like a pair of shorts, ME -- Middle Earth, Uland -- as it is shaped like a U.

Coloring this map could be expressed as follows:

ME ne Shortz
ME ne Uland
Uland ne Shortz

On this input your program should output:

ME=0
Shortz=1
Uland=2

You should conduct some experiments related to the effectiveness and overhead of forward checking. Write these up in a file Experiments.pdf which you also include in your ZIP file.

Point Breakdown